FDL - Nuprl Definition : one-one

Nuprl Definition : one-one

11,40

one-one(A;B;R) ==

x:A, y, z:B. (R(x,y))

(R(x,z))

(y = z)

clarification:

one-one(A;B;R) ==

x:A.

y:B, z:B. (R(x,y))

(R(x,z))

(y = z

Definitions x:A. B(x), P Q, f(a), s = t

FDL editor aliases one-one

Definitions	x:A. B(x), P Q, f(a), s = t
FDL editor aliases	one-one